es:ES, e1, e2:E. loc(e2) = loc(e1)  Id  (null(es-hist{i:l}(es;e1;e2))  (e2 <loc e1)) 

latex

Definitions	t  T, P  Q, Dec(P), x:A. B(x), ES, E, loc(e), Id, Prop, P  Q, (e <loc e'), True, P  Q, P & Q, P  Q, b, es-hist{i:l}(es;e1;e2), False, A, [e, e'], null(as), Top, S  T
Lemmas	es-interval-nil, assert of null, null-map, es-interval wf2, top wf, assert wf, null wf, es-interval wf, es-interval-is-nil, true wf, es-locl wf, Id wf, es-loc wf, es-E wf, event system wf, decidable es-locl